Lambda the Ultimate

I think it used to be that if I
inserted a newline in my post by myself
it would be like regular HTML and would
stay on a single line unless I used
paragraph tags or whatever.

That seems to have gone away, and now
the posts are some strange mixture
of HTML beahviour and not: newlines
appear to turn into <br> which
seems incongruous to me.

In a series of papers, Jean Goubault-Larrecq has established a relationship between modal logic systems and type systems for metaexpressions, i.e. (quasi-)quoted expressions. I will use a pseudo Lisp syntax and furthermore I will write quote for both quote and quasiquote. In such systems, if (has-type (quote x) (quote A)), then (has-type (quote (quote x)) (quote ([] A))), where [] is a modal operator. One can read "([] A)" as "a representation of an A". The unquote is the corresponding destructor.

It appears to me that modal operators are merely syntactic abbreviations for predicates on propositions, i.e., ([] A) is merely an abbreviation for (P (quote A)) where P is some corresponding predicate on propositions. For example, the modal operator in provability logics can be identified with the |- provability predicate: to express that A is provable one can write either (|- (quote A)), or ([] A). A proposition thus has type (quote (|- (quote bool))).

(By the way, if we treat predicates/sets as characteristic functions, then modal operators are really evaluators, and |- with two relands is an evaluator with an environment. A partially applied type-assignment relation (has-type (quote x)) then corresponds to a modal operator [(quote x)] that has a term as a parameter.)

The proof rules rules for minimal logic in their most basic form (with a single proposition instead of a context) look like the following:

(has-type (quote make-x) (quote (|- (quote P)))) 
(has-type (quote make-y) (quote (|- (quote Q))))
; ... other assumptions

(has-type (quote i→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (→ (|- a) (|- b))
                        (|- (quote (→ (unquote a) (unquote b)))))))))
(has-type (quote e→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (|- (quote (→ (unquote a) (unquote b))))
                        (→ (|- a) (|- b)))))))

Now it becomes clear that proof rules are the types of the constructors of the proofs (terms) in a language. For example, (e→ (quote (→ A B)) (quote A) (quote f) (quote x)) denotes (quote (f x)) The first two arguments are there because e→ is polymorphic, but they can be left implicit.

The written representation of an abstraction term is now problematic because the abstraction term contructor i→ takes a function of type (quote (→ (|- (quote A)) (|- (quote B)))) as argument, not a (sub)term. To write down a abstraction term we would have to write the written representation of a function. This implies it is impossible to write down abstraction terms.

We can resort to a trick to be able to write some abstraction terms indirectly. Here the substitution function comes to the rescue. Most generally, subst takes five arguments: (subst (quote A) (quote B) (quote x) (quote M) (quote N)). The two types (quote A) and (quote B) are given because subst is polymorphic and it must be specified what is the type of (quote x) on the one hand and (quote N) and (quote M) on the other hand. I will sometimes leave them implicit as in other situations.

Partially applying subst to four arguments, the resulting term has the required type (quote (→ (|- a) (|- b))). Thus the term (i→ (quote A) (quote B) (subst (quote A) (quote B) (quote x) (quote M))) is correctly typed and is a abstraction term that does what you expect.

This explains the strange shape of λ terms: a λ term is actually a macro (i.e. syntactic abbreviation) for a term that cannot be written, somewhat as follows (the output type b is inferred):

(defmacro λ (x a m))
  (i→ (subst a b x m)))

Note the absense of quotes in the body. Alternatively, we can add a new `λ reduction' rule (the output type b is inferred):

(∀ ... (→λ (quote (λ (unquote x) (unquote a) (unquote m)))
                  (i→ (subst a b x m))))

This explains the shape of the beta reduction rule:

(∀ ... (→β (e→ (quote (λ (unquote a) (unquote x) (unquote m))) n)
               (subst a b x m n)))

This is because this rule is merely a special case of a more general rule for beta reduction:

(∀ ... (→β (e→ (i→ f) n) (f n)))

or, even more generally,

(∀ ... (→β (e→ (i→ f)) f))

or even something like:

(∀ ... (→β (° e→ i→) id))

By the way, the type assignment rules then become:

(has-type (quote t-make-x) (quote (has-type make-x (quote P))))
(has-type (quote t-make-y) (quote (has-type make-y (quote Q))))
; ... other variable declarations
(has-type (quote ti→)
          (quote (∀ ...
                   (→ (→ (has-type x a) (has-type (f x) b))
                      (has-type (i→ f) (quote (→ (unquote a) (unquote b))))))))
(has-type (quote te→)
          (quote (∀ ...
                   (→ (has-type f (quote (→ (unquote a) (unquote b))))
                      (→ (has-type x a) (has-type (e→ f x) b))))))

Does anyone know which OO languages support a-posteriori subtyping? In other words the creation of new subtype relationships between classes without modifying existing classes. Thanks a lot!

Functions are sometimes defined in terms of sets as the binary relation that relates each x to (f x), but this seems fundamentally wrong to me, because sets bear an immediate resemblance to lambda expressions.

1. Lambda abstractions are similar to set comprehensions. Compare {x | M} to (λ x . M) (or {x:A | M} to (λ x:A . M)).
2. Application syntax is identical to predication syntax. Compare (f x) to (f x). (If by (f x) we mean (x ∈ f) or, using prefix, (∋ f x), then ∋ corresponds to the application special operator sometimes written as @.) Note that ∋ and @ are special operators (to use Lisp terminology) not functions or relations. It is sometimes claimed that ∋ is a relation on sets but that cannot be the case because if you define relations using set membership then (∋ x y) means (∋ ∋ ⟨x y⟩), i.e. (∋ ∋ ⟨∋ ⟨x y⟩⟩), ad infinitum, which does not make sense. Rather, ∋ and @ are primitive concepts (special operators).
3. The beta reduction rule holds for both systems. Compare ((λ x . M) N) →_β (subst x M N) to (∋ {x | M} N) →_β (subst x M N).
4. The eta reduction rule holds for both systems. Compare (λ x . (M x)) →_η M to {x | (∋ M x)} →_η M (for x not free in M).

Etc. So I think the proper way to do things is to equate sets and predicates and to define a set as a function that returns a Boolean. I thought I had come up with this but it turns out Church had thought the same thing (calling this function the characteristic function IIRC) and it is also called the indicator function.

Given all this, can somebody tell me why mathematicians keep making a distinction between sets, predicates and their indicator functions (other than historcial reasons)? Why not simply equate sets, predicates and their characteristic functions?

Hello,

I'm proposing a Programming Language Theory WikiProject on the English-language Wikipedia. A WikiProject, for those unfamiliar, is a group of Wikipedia editors who write and edit articles (for the Wikipedia) on specific topics, ensuring consistent quality, formatting, and such.

Note that this is not:

* A WikiSpaces project;
* Competition for, or redundant with, the proposed LTU wiki

Instead, it is a project to improve Wikipedia's coverage of these topics, which is currently spotty. The output of the project will be encyclopedia articles (new or improvements to existing articles) on subjects related to PLT theory.

As such, Wikipedia guidelines will need to be followed; the main ones which apply are:

* Verifiablity--any and all claims must be supported (or at least supportable) by references to the appropriate literature.
* NPOV--all significant sides of controversial issues need to be reflected--and again, attributed to sources outside of Wikipedia. (This does not mean we have to include the opionions of trolls and such--significant means significant). Statements and claims which are opinion or speculation are generally unwelcome, unless they can be externally sourced.
* No original research. This is not the place to discuss original ideas, publish research, or hold discussions on new or novel ideas. Nor is Wikipedia a discussion forum (though discussion relevant to the articles is welcome in the talk pages).

The focus is writing articles for an encyclopedia. (This is why this is not at all a replacement or competition for LtU, or the proposed LTU wiki).

One former Wikipedia policy which used to be in force, but has largely gone by the wayside, is the avoidance of specialist articles and subjects. Wikipedia currently hosts articles--understandable only by specialists in the field--on many topics, such as physics. Original research--as stated above--is out, but technical subjects well-supported in the primarly literature are welcome.

If you're interested, follow the link above (which points to a subpage of my homepage; I'm EngineerScotty on WP) and comment! If don't currently have a WP membership, creating an account is free and easy--the link to do so is at the top of every page on Wikipedia.

Thanks!

I don't like how the blockquote color is in blue, the same color as hyperlinks. Why not keep it black? They already stand out by being indented, having the bar in front, and being in italics!

Stanford University, Oct 24, 2005

The nice thing about a language that takes hold is that you can work with it again and again. In 30 years we have built Smalltalk systems with quite different constraints. This talk will examine a few of these, and show how tricks of the trade can be applied to enhance one aspect or another and, frequently, to make real progress.

The topic "Choice of OS of LtU readers" asked the wrong question and hence got a sequence of boring I use Linux or I use Windows answers. So let's ask the Right Question.

What new OS shows most promise of ...
a) Doing "The Right Thing" (in the Programming Language Designers overwhelmingly over developed Sense of Right),
b) Being usable in the near term,
and, as such, merits our attention, support and dual boot disk space?

A quick bit of Googling and weeding of the results turns up...

• Brix - Everything must be compiled to a "safe" meta language called Tetra

• Inferno (A Plan 9 derivative with "safe" language Limbo.)
• Plan 9 - Everythings a file, and a file is just a stream of bytes, and who cares where network wise where any thing really is.
• Unununium

Any other suggestions / commentary on these OS's most welcome.

Instead of emphasizing the what, I want to emphasize the how part: how we feel while programming. That's Ruby's main difference from other language designs. I emphasize the feeling, in particular, how I feel using Ruby. I didn't work hard to make Ruby perfect for everyone, because you feel differently from me. No language can be perfect for everyone. I tried to make Ruby perfect for me, but maybe it's not perfect for you. The perfect language for Guido van Rossum is probably Python. -Matz.

Has anybody, then, made systems which might some day convert any language into any other language in a clean fashion, so that I can write in Alice ML and you can modify it in Java? Personally, I think it is obvious that even if such transmogrification were avaialble, it wouldn't always help a heck of a lot because the density of any given region of code can change like 100x. Not to mention that I guess any Turing-esque equivalency doesn't take into consideration the differences in runtime.

Another take on this: Why aren't there programming language generators / wizards which ask me a series of 20 questions ("do you prefer static or dynamic typing?" - i'd like to be able to answer 'both', of course) and then spit out a framework language (including debugger!) for me? (And under the covers everything gets converted to/from XML so we can individually put the curly braces - if any - wherever we prefer.)

Here you can find some amazing(!) peer reviews of a few famous papers (by Dijkstra, Turing, etc.).